COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	bird.3[f82,jmc]		The reasoning itself
C00015 00003	The result of circumscribing  is-ostrich  will be
C00016 ENDMK
C⊗;
bird.3[f82,jmc]		The reasoning itself

	The predicates occuring in the above sentences are
is-ostrich, is-penguin, dead, is-rock,  is-canary,  is-bird,  can-fly,
and  prev-can-fly.  They
are all unary, and this is one of the ways in which the Tweety
problem is untypically simple.  As it turns out, common sense
will tell us that all the predicates are to be circumscribed,
but some with higher priority than others.  Also, as it turns out,
the priority matters only in comparing  prev-can-fly  and  can-fly;
in every other case, circumscribing some of the
predicates does not limit the circumscription of the others.  Let
us consider the predicates individually.

	is-ostrich  appears only in the sentences  is-ostrich Joe,
∀x.is-ostrich x ⊃ is-bird x, and  ∀x.is-ostrich x ⊃ prev-can-fly x.
When we circumscribe  is-ostrich  in the conjunction of all the
premisses, the circumscription formula takes the form

(1)	∀io.[io Joe ∧ (∀x.io x ⊃ is-bird x) ∧ (∀x.io x ⊃ prev-can-fly x)
∧ <conjuncts of assumptions not involving  is-ostrich>
∧ (∀x.io x ⊃ is-ostrich x) 
	⊃ ∀x.is-ostrich x ⊃ io x].

We have written it as a second order formula and used  io  as the
name of the predicate variable replacing  is-ostrich  in the circumscription.
Here we have regarded all the other predicates as parameters rather
than as variables.  We now put

	∀x. io(x) ≡ x = Joe.

The formula (1) then simplifies to

(2)	is-bird Joe ∧ prev-can-fly Joe ∧ <above-mentioned conjuncts> ∧ is-ostrich Joe 
	⊃ (∀x.is-ostrich x ⊃ x = Joe).

The sentences on the left hand side all follow from the assumptions, so
we end up with

(3)	∀x.is-ostrich x ⊃ x = Joe.

	Since we have regarded all the other predicate symbols as parameters,
and therefore have not used them in circumscribing  is-ostrich,  the
result that Joe is the only ostrich has a certain unconditional character.

	Circumscribing  is-rock  and  is-canary  proceeds exactly
analogously.  Henry is the only rock, and Tweety is the only canary.
If we circumscribe  is-bird  holding all else as parameters, we will
get that the only birds are ostriches, penguins
and canaries.  Combining this with
the previous results leads to the conclusion that Tweety and Joe are
the only birds.  The predicates  dead  and  is-penguin  are even simpler;
since nothing is asserted to be dead or a penguin,
circumscription makes  dead x  is-penguin x  always false.

	We aren't done yet, because we haven't yet inferred that
Joe and Tweety and Henry are distinct.  This can be inferred in
two ways.  The first is that it is a part of common sense knowledge
that ostriches, canaries and rocks are distinct.  It is, but it seems
doubtful that humans store pairwise distinctness axioms for all the
species and kinds of objects.  It would also be ineffecient for
AI systems; it is difficult to imagine that when a new species is
introduced, a disjointness axiom with each previously known species
should also be introduced.  We need some variant of Reiter's (1979)
"unique names hypothesis", which assumes that objects with distinct
names are distinct unless there is evidence to the contrary.  Reiter
treats this as a special kind of non-monotonic inference, but
circumscription seems better, since it makes it a defeasible presumption.

	We suppose that the system can directly tell when two names
are distinct, i.e. "Tweety" ≠ "Joe", "is-ostrich" ≠ "is-canary"
and "is-ostrich" ≠ "is-bird" are all immediately accepted by the
reasoning system.  In a proof-checker this would be done by an
"attachment", and there are several ways it might be done in
a logical problem-solver, but it is beyond the scope of this paper
to discuss them.  We then use an axiom

∀name1 name2 obj1 obj2. names(name1,obj1) ∧ names(name2, obj2)
	∧ name1 ≠ name2 ∧ ¬same(obj1,obj2) ⊃ obj1 ≠ obj2,

and we circumscribe the sentence  same(obj1, obj2).  In the present
problem we can either circumscribe  same(is-ostrich, is-canary),  which
requires a weak form of second order logic or we can get it down
to first order logic by using an apply predicate, e.g. we define

	∀x. is-ostrich x ≡ applies("is-ostrich", x).

	The alternate way of getting  Joe ≠ Tweety  is to use one
of the above-mentioned unique-names methods applied to the individual
names "Joe" and "Tweety" rather than to the species.
Presumably both should be available in
in AI systems that do common sense reasoning, because
both methods are used in human common sense reasoning.

	Perhaps we should include a dead canary in our scenario,
since the predicate  dead x  certainly overlaps the species, but
this paper is long enough already.

	prev-can-fly  and  can-fly  are the remaining predicates.  The
results of circumscribing  is-ostrich,  is-canary,  and  is-bird
do not depend on any assumptions about  prev-can-fly  and  can-fly.
The common sense conclusion we want is that a bird  x  can fly unless
one of the conditions allowing the inference  prev-can-fly x  applies.
This may be accomplished by circumscribing  prev-can-fly  with  can-fly
treated as a variable.  The circumscription formula is then

∀pcf cf.(∀x.isbird x ∧ ¬pcf x ⊃ cf x) ∧ (∀x.is-ostrich x ⊃ pcf x)
∧ (∀x.is-penguin x ⊃ pcf x)
∧ (∀x.dead x ⊃ pcf x) ∧ (∀x.pcf x ⊃ ¬cf x) ∧ ∀x.(pcf x ⊃ prev-can-fly x)
	⊃ ∀x.(prev-can-fly x ⊃ pcf x).

We then substitute

	∀x.pcf x ≡ is-ostrich x ∨ is-penguin x ∨ dead x

and

	∀x.cf x ≡ is-bird x ∧ ¬is-ostrich x ∧ ¬is-penguin x ∧ ¬dead x.

It is then easily verified that with the help of the assumptions,
all the conjuncts on the left hand side of (4) are satisfied,
and we get the conclusion

	∀x.prev-canfly x ⊃ is-ostrich x ∨ is-penguin x ∨ dead x.

Since our previous circumscriptions tell us that the only ostrich
is Joe and nothing is a penguin or dead and that Tweety is not
Joe, we get

	¬prev-can-fly Tweety

and finally the desired

	can-fly Tweety.

	We can also circumscribe  can-fly,  but this should be done
with  prev-canfly  as a parameter rather than as a variable.
The circumscription formula is then

∀cf.(∀x.isbird x ∧ ¬prev-can-fly x ⊃ cf x) ∧ (∀x.is-ostrich x ⊃ prev-can-fly x)
∧ (∀x.is-penguin x ⊃ prev-can-fly x)
∧ (∀x.dead x ⊃ prev-can-fly x) ∧ (∀x.prev-can-fly x ⊃ ¬cf x)
 ∧ ∀x.(cf x ⊃ can-fly x)
	⊃ ∀x.(can-fly x ⊃ cf x).

Into it we can substitute

	∀x.cf x ≡ x=Tweety,

and using the axioms and the previously established results about  prev-can-fly,
we can prove

	∀x.can-fly x ≡ x=Tweety.

The circumscription is somewhat redundant except for Henry the rock,
because the others are all caught by the direct law

	∀x.prev-can-fly x ⊃ ¬can-fly x.

	In obtaining these results, it was essential that  prev-can-fly
be circumscribed with higher priority than  can-fly,  i.e. that  can-fly
be variable in circumscribing  prev-can-fly  and that  prev-can-fly  be
a parameter in circumscribing  can-fly.  If each were taken as variable
in circumscribing the other, a contradiction would be reached, because
we could take  prev-can-fly Tweety  to be true in the latter.  If each
were taken as a parameter in the circumscription of the other, we would
not arrive at a definite conclusion concerning Tweety - only the
disjunction  prev-can-fly Tweety ∨ can-fly Tweety.

	The most straightforward way of
ascribing priorities is to include a partial ordering of predicates in
the common sense data base and have the reasoning program use this
ordering.  This will surely work in many cases, but most likely it will
turn out that the ordering may depend on facts, and this suggests using
second order or metalinguistic formulas included as ordinary facts
that can be derived.  At present writing, I have no examples to serve
as a guide.

	Like all logical deductions, this one is long when spelled out
in detail, but computers can do them fast enough.
The result of circumscribing  is-ostrich  will be

	∀x.is-ostrich x ≡ x = Joe,

regardless of whether we take into account only the first of these
sentences or the whole lot.  This is because  is-ostrich  only
appears in the left hand side of implications in the other sentences,
so they can't interfere with making  is-ostrich  as false as possible.